/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package expression;

import core.Node;
import core.UnsatException;
import domain.Domain;

/**
 *
 * @author ddoose
 */
public class VarInDomain extends IntExpr {
    private Domain reducedDomain;
    
    public VarInDomain(Node n, Domain d) {
        super(n);
        reducedDomain = d;
        current = Domain.BOOLEAN;
        target = Domain.BOOLEAN;
    }

    public VarInDomain(Node n, Variable v, Domain d) {
        super(n, v);
        reducedDomain = d;
        current = Domain.BOOLEAN;
        target = Domain.BOOLEAN;
    }

    public boolean same(IntExpr i) {
        return (i instanceof VarInDomain) && reducedDomain.equals(((VarInDomain)i).reducedDomain) && sameParameters(i);
    }
    
    public void eval() throws UnsatException {
        Variable variable = (Variable)node.getIntExpr(getParameters().get(0));
        Domain inter = reducedDomain.inter(variable.current);
        
        // FALSE
        if (inter.isEmpty()) {
            reduceCurrent(Domain.FALSE);
        }
        // TRUE
        else if (inter.equals(variable.current)) {
            reduceCurrent(Domain.TRUE);
        }
    }

    public void propagate() throws UnsatException {
        Variable variable = (Variable)node.getIntExpr(getParameters().get(0));
        
        // TRUE
        if (target.isTrue()) {
            variable.reduceTarget(reducedDomain);
        }
        // FALSE
        else if (target.isFalse()) {
            variable.reduceTarget(reducedDomain.comp());
        }
    }
    
    public boolean reduce() {
        // FALSE
        if (current.isFalse()) {
            Value v = node.createValue(0);
            node.replaceIntExpr(id, v.getId());
            return true;
        }
        // TRUE
        if (current.isTrue()) {
            Value v = node.createValue(1);
            node.replaceIntExpr(id, v.getId());
            return true;
        }
        return false;
    }
    
    public VarInDomain clone(Node n) {
        VarInDomain vid = new VarInDomain(n, reducedDomain);
        vid.clone(this);
        return vid;
    }

    public String toString() {
        Variable variable = (Variable)node.getIntExpr(getParameters().get(0));
        return "(" + variable + " in " + reducedDomain +")";
    }
    
    public String pretty() {
        return id + "\t" + current + "\t" + target + "\t" + toString();
    }
}
